perm filename BELIEF[F83,JMC] blob sn#732496 filedate 1983-11-26 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	belief[f83,jmc]		Axioms for persistence of belief
C00004 ENDMK
C⊗;
belief[f83,jmc]		Axioms for persistence of belief

We want to use  ab  and circumscription to formalize the persistence
of unchallenged beliefs.

1.	∀p t.¬ab aspect1(p,t) ⊃ ¬believe(p,t)
Normally a proposition isn't believed.

2.	∀p t t1.believed(p,t1) ∧ t1 < t ∧ (∀t2.t1≤t2≤t ⊃ ¬believed(not p,t2))
		⊃ ab aspect1(p,t)
(1) doesn't apply to propositions that were previously believed
and whose denial wasn't believed more recently.

3.	∀p t t1.believed(p,t1) ∧ t1 < t ∧ (∀t2.t1≤t2≤t ⊃ ¬believed(not p,t2))
		∧ ¬ab aspect2(p,t)
	⊃ believed(p,t)
Under the same conditions as (2), a proposition normally is believed.

	These axioms presume that  ab z  is to be circumscribed, but
since circumscription, as we presently know it, is expensive computationally,
we really propose that the same effect be obtained in some less
expensive way.  For now, however, circumscription defines the logic.